Module code | COS 740 |
Qualification | Postgraduate |
Faculty | Faculty of Engineering, Built Environment and Information Technology |
Module content | This module focuses on formally specifying systems by means of Event-B. In this formalism, complex systems are specified as abstract machines which are characterised mainly by pre-conditions and post-conditions. From initially highly abstract machines, for which only very few features are stipulated, the module proceeds to more concrete machines which are richer in the details of their features. Such a "refinement", which eventually approaches a form that is almost implementable, is acceptable if it is logically consistent with the abstract machine with which the entire formal modelling process had started. Already available proof tools (for example: Rodin, or Pro-B) will be applied practically in order to demonstrate the validity of those refinement relations. |
Module credits | 15.00 |
NQF Level | 08 |
Programmes | |
Prerequisites | No prerequisites. |
Contact time | 2 lectures per week |
Language of tuition | Module is presented in English |
Department | Computer Science |
Period of presentation | Semester 1 or Semester 2 |
Copyright © University of Pretoria 2024. All rights reserved.
Get Social With Us
Download the UP Mobile App